%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             Languages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% new commands, new type systems (May 28)

\newcommand{\destroy}[1]{\mathsf{kill}[#1]}
\newcommand{\migrate}[2]{\mathsf{move}[#1, #2]}
\newcommand{\linear}{\mathtt{lin}}


\newcommand{\ioname}{\mathcal{IO}}
\newcommand{\luname}{\mathcal{LU}}

\def\subst#1#2{[\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}]}
\newcommand{\deff}{\triangleq}

\newcommand{\evol}[1]{\ensuremath{\mathcal{E}^{\mathtt{#1}}}\xspace}

\newcommand{\outC}[2]{{\overline{#1}}( #2 )}  % output
\newcommand{\outCn}[2]{{#1}( #2 )}  % output
\newcommand{\inC}[2]{#1(#2)}  % output
\newcommand{\throw}[2]{{#1}\langle\!\langle#2\rangle\!\rangle}  % throw
\newcommand{\alte}{\ensuremath{\, [\!] \,}} % for branching
\newcommand{\catch}[2]{{#1}(\!(#2)\!)}  % throw
\newcommand{\qua}{\ensuremath{\mathsf{q}}}  % 
\newcommand{\qual}{\ensuremath{\mathsf{lin}}}  % 
\newcommand{\quau}{\ensuremath{\mathsf{un}}}  % 
\newcommand{\addelta}{\ensuremath{\uplus}}  % 
\newcommand{\midelta}{\ensuremath{\ominus}}  % 
\newcommand{\compat}{\ensuremath{\asymp}}  % 
\newcommand{\D}{\ensuremath{\Delta}}  % 
\newcommand{\T}{\ensuremath{\Theta}}  % 
\newcommand{\subt}{\ensuremath{\preceq}}  % 
\newcommand{\intpr}{\ensuremath{\sqsubseteq}\xspace}  % 

%%% new conventions
\newcommand{\INT}{\ensuremath{\mathcal{I}}}  % 
\newcommand{\unres}{\!\uparrow^{\quau}}
%\newcommand{\unres}{\mathsf{UR}}
\newcommand{\INTdyn}{\INT_{dyn}}
\newcommand{\ST}{\ensuremath{\alpha}}  % 
\newcommand{\STT}{\ensuremath{\beta}}  % 
\newcommand{\ActS}{\ensuremath{\Delta}}
\newcommand{\cha}{\ensuremath{\kappa}}
\newcommand{\ovl}[1]{\ensuremath{\overline{#1}}}
\newcommand{\arrive}[1]{\ensuremath{\mathsf{arrive}(#1)}}

\newcommand{\locf}[1]{\ensuremath{\mathbf{\mathrm{#1}}}}
\newcommand{\evc}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\locc}[1]{\ensuremath{C\big\{#1\big\}}}
\newcommand{\loccp}[1]{\ensuremath{C_1\big\{#1\big\}}}
\newcommand{\locd}[1]{\ensuremath{D\big\{#1\big\}}}
\newcommand{\locdp}[1]{\ensuremath{D_1\big\{#1\big\}}}
\newcommand{\locdb}[1]{\ensuremath{D\Big\{#1\Big\}}}

\newcommand{\component}[4]{#1^{#2} [#4]   }  %a^n[P]
\newcommand{\scomponent}[2]{#1[#2]   }  %a[P]
\newcommand{\scomponentbig}[2]{#1\big[#2\big]   }  %a[P]
\newcommand{\compo}[3]{  \component{#1}{#2}{}{#3}   } 
\newcommand{\bigcomponent}[4]{#1^{#2} \big[#4\big]   }  %a^n[P]
\newcommand{\bigscomponent}[2]{#1 \big[#2\big]   }  %a^n[P]

\newcommand{\adaptn}[2]{\ensuremath{\mathsf{upd}(#1, #2)}}
%\newcommand{\adapt}[3]{\mathsf{upd}(#1, #2( \mathsf{#3}))} OLD VERSION
%\newcommand{\adapt}[3]{#1\{\lambda #3. #2\}} %
\newcommand{\adapt}[3]{#1\{(#3).#2\}} %

\newcommand{\nadapt}[2]{#1\{#2\}} %
\newcommand{\nadaptbig}[2]{#1\big\{#2\big\}} %

% Recursion and Update Variables
\newcommand{\recu}{\ensuremath{\mathsf{rec}}}
\newcommand{\rv}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\uv}[1]{\ensuremath{\mathsf{#1}}}

\newcommand{\mupdate}[4]{{#1}^{#3}_{#4}\big\{#2\big\}} % a{P}
\newcommand{\update}[4]{{#1}\{#4(\mathsf{#2}{:}#3)\} } % a{P}
\newcommand{\updated}[5]{{#1}^{#3}_{#4}\{#5(\mathsf{#2})\} } % a{P}
\newcommand{\quicktype}{\textsc{Int}}
\newcommand{\intf}[1]{\INT_{[#1]}}

\newcommand{\para}{\mathord{\;\boldsymbol{|}\;}}

%\newcommand{\update}[4]{{#1}\{#4\} } % a{P}
\newcommand{\up}[1]{\hat{#1}}
\newcommand{\loc}[1]{\check{#1}}

\newcommand{\nopen}[2]{\mathsf{open}\,#1\,(#2)}
\newcommand{\nopena}[2]{#1(#2)}
%\newcommand{\repopen}[2]{\text{\textbf{!}} \,#1(#2)}
\newcommand{\repopen}[2]{\ast#1(#2)}
\newcommand{\nopenr}[2]{\overline{#1}(#2)}
\newcommand{\open}[1]{\mathsf{open}(#1)}
\newcommand{\close}[1]{\mathsf{close}\,(#1)}
\newcommand{\closeact}{\mathsf{close}}
\newcommand{\que}[2]{\ensuremath{#1\lfloor #2\rfloor}}


\newcommand{\restr}[2]{(\nu #1 )#2}

\newcommand{\ifte}[3]{\mathsf{if}~ #1 ~\mathsf{then}~ #2 ~\mathsf{ else }~#3}
\newcommand{\ift}[2]{\mathsf{if}~ #1 ~\mathsf{then}~ #2}

\newcommand{\branch}[2]{#1\triangleright \{#2\}}
\newcommand{\branchbig}[2]{#1\triangleright \big\{#2\big\}}
\newcommand{\select}[2]{#1\triangleleft #2}

\newcommand{\mycase}[4]{\mathsf{case}\,#1\,\mathsf{of}\,\{(#2):#3\}_{#4}}

\newcommand{\rec}[2]{\mathrm{rec} (#1).#2}



\newcommand{\conc}[2]{\langle #1 \rangle  #2}

\def\nil{{\boldsymbol 0}} %nil = 0

\def\sub#1#2{[\raisebox{.5ex}{\small${#1}$}\! / \mbox{\small${#2}$}]} %substitution

\newcommand{\act}{\eta}


% Command for context
\newcommand{\fillcon}[2]{\ensuremath{#1\langle\!\langle #2 \rangle\!\rangle}}  % 1 << 2 >>

\newcommand{\CStr}{\ensuremath{\mathsf{St}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             types
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\name}{\mathrm{name}}
\newcommand{\ch}{\mathrm{ch}}
\newcommand{\var}{\mathrm{var}}

\newcommand{\dom}[1]{\mathrm{dom}(#1)}

\newcommand{\capab}{\tau}

\newcommand{\env}[2]{#1 \,;\, #2}
%\newcommand{\type}[2]{#1;#2}
%\newcommand{\type}[2]{#1 \,\circ\, #2}
\newcommand{\type}[2]{#1;#2}
\newcommand{\judgement}[5]{\env{#1}{#2} \vdash #3 \triangleright \type{#4}{#5}}
\newcommand{\judgebis}[3]{#1 \vdash #2\triangleright #3}
\newcommand{\typecontx}[3]{\mathrm{tp}^{#2,#3}(#1)}


\newcommand{\tin}[1]{?(#1)}
\newcommand{\tout}[1]{!(#1)}

\newcommand{\inter}[3]{\langle #1 : #2, #3\rangle}
\newcommand{\restrint}[2]{\langle [#1 : #2], 1\rangle}



\newcommand{\typing}[3]{#1 \vdash #2 \triangleright  #3}
\newcommand{\bool}{\mathsf{bool}}
\newcommand{\true}{\mathtt{true}}
\newcommand{\false}{\mathtt{false}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             Arrows and LTSs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\rulename}[1]{\textsc{$\langle$#1$\rangle$}}
\newcommand{\srulename}[1]{{\small \textsc{(#1)}}}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\proj}[2]{\ensuremath{#1\downarrow#2}}

\newcommand{\pired}{\longrightarrow} %-->

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             Shortcuts
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%separator
%\newcommand{\sepr}{ \  \mid \ }
\def\sepr{\; \mbox{\large{$\mid$}}\;}
%\def\midd{\; \; \mbox{\Large{$\mid$}}\;\;} %% davide's original macro

\newcommand{\til}[1]{\widetilde{#1}}

\newcommand{\andalso}{\quad\quad}


\newcommand{\out}[1]{\outC{#1}}%output nel processo



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             Encodings and MM
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Encoding
\newcommand{\encp}[2]{\llbracket #1 \rrbracket_{#2}}

% Encoding of numbers for the MM encoding:
\newcommand{\on}{(\!|}
\newcommand{\cn}{|\!)}
\newcommand{\encn}[2]{\on #1 \cn_{#2}}
\newcommand{\encu}[1]{\on #1 \cn}


\newcommand{\mmn}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\mmss}{MMs\xspace}
\newcommand{\mm}{MM\xspace}

\newcommand{\minskred}{\longrightarrow_{\textrm{\textsc{M}}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             WSTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newcommand{\fb}[2]{\mathtt{FB}_{#2}(#1)}

\newcommand{\seqsub}{\mathtt{ss}}
\newcommand{\subp}{\seqsub}
\newcommand{\procleq}{\preceq}
\newcommand{\Tree}{\mathsf{Tr}}
\newcommand{\pbs}{\mathtt{pb}^*}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             Comments
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\todo}[1]{\textcolor{red}{\textbf{#1}}}
\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\green}[1]{\textcolor{green}{#1}}
\newcommand{\jp}[1]{\textcolor{blue}{[JP says: #1]}}


\newcommand{\unf}[1]{\ensuremath{\mathbf{unfold}(#1)}}
\newcommand{\mcc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\ty}{\ensuremath{T}}
\newcommand{\tyy}{\ensuremath{S}}
\newcommand{\bsub}{\ensuremath{\leq_{\mathtt{B}}}\xspace}
\newcommand{\csub}{\ensuremath{\leq_{\mathtt{C}}}\xspace}
\newcommand{\cdual}{\ensuremath{\,\bot_{\mathtt{C}}}\,}
